\begin{tabbing}
es{-}dt($l$; ${\it da}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$compose{-}fpf(\=($\lambda$$k$.if isrcv($k$)\+
\\[0ex]then if eq\_lnk(lnk($k$); $l$) then inl tag($k$)  else inr $\cdot$  fi 
\\[0ex]else inr $\cdot$ 
\\[0ex]fi );
\\[0ex]($\lambda$${\it tg}$.rcv($l$,${\it tg}$));
\\[0ex]${\it da}$)
\-
\end{tabbing}